decide(Lean 4)

decide(Lean 4)

Lean 4でDecidable型クラスのインスタンス(instance)を書いているものはいい感じに証明を進めれるようになっている

Decidableは命題に関する型クラス

Decidable Propositions (決定可能命題)

decideタクティクを書くと一気に証明が進む

code:memo

example : 10 < 5 ∨ 1 > 0 := by

decide

example : ¬ (True ∧ False) := by

decide

example : 10 * 20 = 200 := by

decide

theorem ex : True ∧ 2 = 1+1 := by

decide

-- theorem ex : True ∧ 2 = 1 + 1 :=

-- of_decide_eq_true (Eq.refl true)

#check @of_decide_eq_true

-- ∀ {p : Prop} Decidable p, decide p = true → p

#check @decide

-- (p : Prop) → Decidable p → Bool

DecidableEqは

確認用

Q. decide(Lean 4)